/*********************************************************************
Author: Roberto Bruttomesso <roberto.bruttomesso@unisi.ch>

MiniWrapper -- Copyright (C) 2008, Roberto Bruttomesso

MiniWrapper is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.

MiniWrapper is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
GNU General Public License for more details.

You should have received a copy of the GNU General Public License
along with MiniWrapper. If not, see <http://www.gnu.org/licenses/>.
*********************************************************************/

%{

#include <cstdio>
#include <cstdlib>
#include <cassert>
#include "Solver.h"
#include <map>
#include <string>

using namespace std;

struct parser_data
{
  Solver S;
  map< string, Var > string_to_var;
  map< Var, string > var_to_string;
};

#define YYPARSE_PARAM parm

extern int yylineno;
extern int yylex( );

void addLit( struct parser_data &, char * name, bool negate );
void addCurrentClause( struct parser_data & );

void yyerror( char * s )
{
  printf( "%d: %s\n", yylineno, s );
  exit( 1 );
}

vec< Lit > current_clause;

/* Overallocation to prevent stack overflow */
#define YYMAXDEPTH 1024 * 1024

%}

%union
{
  char  * str;
}

%token TK_STR TK_NEGATION TK_END_CLAUSE

%type <str> TK_STR

%start top

%%

top: all
   ;

all: all literal
   | all end_clause
   | literal
   | end_clause
   ;

literal: TK_NEGATION TK_STR
         { addLit( *((struct parser_data *) parm), $2, true ); free( $2 ); }
       | TK_STR
         { addLit( *((struct parser_data *) parm), $1, false ); free( $1 ); }
       ;

end_clause: TK_END_CLAUSE
	    { addCurrentClause( *((struct parser_data *) parm) ); }
          ;

%%

//=======================================================================================
// Auxiliary Routines

void addLit( struct parser_data & data, char * name, bool negate )
{
  // Create new variable if necessary
  if ( data.string_to_var.find( name ) == data.string_to_var.end( ) )
  {
    data.string_to_var[ name ] = data.S.newVar( );
    data.var_to_string[ data.string_to_var[ name ] ] = name;
  }

  Var v = data.string_to_var[ name ];

  current_clause.push( Lit( v, negate ) );
}

void addCurrentClause( struct parser_data & data )
{
  data.S.addClause( current_clause );
  current_clause.clear( );
}
